minus(x, y) → cond(ge(x, s(y)), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
minus(x, y) → cond(ge(x, s(y)), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
MINUS(x, y) → COND(ge(x, s(y)), x, y)
COND(true, x, y) → MINUS(x, s(y))
GE(s(u), s(v)) → GE(u, v)
MINUS(x, y) → GE(x, s(y))
minus(x, y) → cond(ge(x, s(y)), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MINUS(x, y) → COND(ge(x, s(y)), x, y)
COND(true, x, y) → MINUS(x, s(y))
GE(s(u), s(v)) → GE(u, v)
MINUS(x, y) → GE(x, s(y))
minus(x, y) → cond(ge(x, s(y)), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
GE(s(u), s(v)) → GE(u, v)
minus(x, y) → cond(ge(x, s(y)), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GE(s(u), s(v)) → GE(u, v)
The value of delta used in the strict ordering is 85/16.
POL(GE(x1, x2)) = x_1 + (13/4)x_2
POL(s(x1)) = 5/4 + (15/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
minus(x, y) → cond(ge(x, s(y)), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
MINUS(x, y) → COND(ge(x, s(y)), x, y)
COND(true, x, y) → MINUS(x, s(y))
minus(x, y) → cond(ge(x, s(y)), x, y)
cond(false, x, y) → 0
cond(true, x, y) → s(minus(x, s(y)))
ge(u, 0) → true
ge(0, s(v)) → false
ge(s(u), s(v)) → ge(u, v)